Skip to content

Honor the project-declared EVM version + Yul-steps escalation rung - #83

Open
shellygr wants to merge 2 commits into
masterfrom
shelly/honor-evm-version
Open

Honor the project-declared EVM version + Yul-steps escalation rung#83
shellygr wants to merge 2 commits into
masterfrom
shelly/honor-evm-version

Conversation

@shellygr

Copy link
Copy Markdown
Contributor

Motivation

Projects can pin an EVM target older than solc's default (evmVersion: "paris" vs the shanghai default of solc >=0.8.20). The difference is not cosmetic: shanghai codegen can fail with YulException stack-too-deep where the declared target compiles, besides producing bytecode for a different target than the project deploys. Autosetup never read the declared version — a corpus project failed compilation analysis in all three PR #66 validation sweeps purely because of this (isolated experimentally: with the declared paris, every solc/optimizer/Yul-steps combination compiles; without it, none does).

Changes

Honor the declared EVM version end-to-end

  • Parse foundry.toml evm_version (incl. profile merge) and hardhat settings.evmVersion; emit scalar solc_evm_version from the shared build-system conf builder.
  • Workaround manager seeds the declared scalar into a total solc_evm_version_map (certora-cli forbids scalar+map together and requires maps to cover every file), collapsing back to the scalar on finalize. The cancun workaround now overrides only the detected contract while the rest keep the declared version.
  • New reactive invalid_evm_version workaround: if solc rejects the declared name ("Invalid EVM version requested." — same text for unknown and too-new names), drop the setting and fall back to solc defaults. No solc-version/EVM-name table to maintain: the compiler is the authority.
  • Merged-conf reconciliation (removal propagation, map-supersedes-scalar with totality fill) + solc_evm_version_map fill in sync_compiler_maps_with_files for files injected after compilation analysis; solc_evm_version joins fixconf's strippable low-priority keys.

Hardhat config extractor: survive moduleResolution: nodenext
The ts-node registration forces module: commonjs; a project tsconfig pinning moduleResolution: "nodenext" then fails TS5110 even in transpileOnly mode — silently degrading the WHOLE hardhat config (solc version, optimizer, viaIR, evmVersion) to defaults. Now overrides moduleResolution: node alongside.

Yul ladder: try solc's default Yul steps before relaxing autofinders
With optimizer + via-ir, certoraRun substitutes finder-friendly Yul steps (full inliner removed). These give less stack relief than solc's own pipeline and can themselves cause stack-too-deep in functions the default pipeline compiles (isolated: fails under the substitute steps at any runs value, compiles under strict_solc_optimizer). New escalation rung between adding the optimizer and relaxing the autofinder assertion.

Validation

  • 251 unit tests pass (-m 'not expensive'), pyright clean. New tests: foundry/hardhat evm_version parsing, seeding/normalize round-trips, invalid-version drop, cancun+declared reconciliation, merged-conf helper, sync fill, strict-steps rung ordering.
  • End-to-end: both corpus contracts of the motivating project now complete compilation analysis (previously failed in all three sweeps after ~21 min of futile ladder walking each). Observed ladder: declared paris honored → stack-too-deep → +optimizer → +strict_solc_optimizer → success, with the autofinder assertion never relaxed.

🤖 Generated with Claude Code

Projects can pin an EVM target older than solc's default (evmVersion "paris"
vs the shanghai default of solc >=0.8.20); shanghai codegen can fail with
YulException stack-too-deep where the declared target compiles, besides
producing bytecode for a different target than the project deploys. Autosetup
never read the declared version. Three fixes:

- Honor the declared EVM version: parse foundry.toml evm_version (with profile
  merge) and hardhat settings.evmVersion; emit scalar solc_evm_version. The
  workaround manager seeds it into a total solc_evm_version_map (the prover
  forbids scalar+map and requires maps to cover every file), collapsing back
  on finalize; the cancun workaround overrides only the detected contract. A
  reactive invalid_evm_version workaround drops the setting when solc itself
  rejects the name ("Invalid EVM version requested.") - no version table.
  Merged-conf reconciliation, map fill in sync_compiler_maps_with_files, and
  fixconf strippable-key coverage included.

- Hardhat config extractor: ts-node registration now overrides
  moduleResolution "node" alongside module "commonjs" - a project tsconfig
  pinning "nodenext" hit TS5110 even in transpileOnly mode and silently
  degraded the whole hardhat config (solc version, optimizer, viaIR,
  evmVersion) to defaults.

- Yul ladder: with optimizer + via-ir, certoraRun substitutes finder-friendly
  Yul steps that give less stack relief than solc's own pipeline and can
  themselves cause stack-too-deep. New escalation rung sets
  strict_solc_optimizer (solc's default Yul steps) before the last resort
  relaxes the autofinder assertion.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
@shellygr
shellygr force-pushed the shelly/honor-evm-version branch from 46379c5 to 4974b1b Compare July 17, 2026 19:09
Conflict resolution highlights, reconciling the branch with #88/#102/#105/#107:

- _seed_compile_maps: master's setdefault-fold style extended to the declared
  solc_evm_version (folds into a pre-existing map as the default for uncovered
  contracts; seeded only when declared — absence means each solc's default,
  which a map entry cannot express).
- The strict-Yul-steps rung and the relax-autofinders last resort are re-gated
  on master's map-aware _yul_optimizer_pending (the pre-#88 scalar check never
  fired in solc_optimize_map mode); ladder remains add-optimizer -> solc
  default Yul steps -> relax autofinder assertion, one rung per pass.
- get_build_system_config_dict_with_updates: _reconcile_evm_version_keys runs
  BEFORE drop_scalars_superseded_by_maps — the helper expands the declared
  scalar into the map's missing entries, impossible once the scalar is dropped.
- update_evm_version_map_for_contract added beside #105's
  update_optimize_map_for_contract and wired into
  _update_compiler_maps_for_new_contracts, so contracts added after
  compilation analysis keep the evm map total.
- Both parents' appended test sections kept; the two #88 optimize-map ladder
  tests updated for the strict-steps rung (escalation now passes through
  strict_solc_optimizer, and enabling map entries no longer jumps straight to
  relaxing the autofinder assertion).

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant